$\forall$$A$,$B$:Type, $f$:($A$$\rightarrow$$B$). constant\_function($f$; $A$; $B$) $\in$ prop\{i:l\}